{-# LANGUAGE ScopedTypeVariables #-}

module Z where

import Prelude ()

data Lemma a = Equals a a
(===) = Equals
infix 1 ===

data Bool = True | False
data Nat  = Zero | Suc Nat

prop_tmp1 :: (Nat -> Bool) -> Nat -> [Nat] -> Lemma [Nat]
prop_tmp1 p x xs =
  case p x of
    False -> filter p xs === filter p (xs ++ [x])


-- Type class for equality

class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  
  x == y = not (x /= y) 
  x /= y = not (x == y)
 
prop_eq_eq_ref x = x == x === True
prop_eq_eq_sym x y = 
  case x == y of
    True -> 
      y == x === True
prop_eq_eq_trn x y z =
  case x == y of
    True -> 
      case y == z of
        True -> 
          x == z === True
          
{-# INLINE prop_eq_eq_sym #-}
{-# INLINE prop_eq_eq_ref #-}
{-# INLINE prop_eq_eq_trn #-}

  
-- Type class for totally ordered data types

class Eq a => Ord a where
  (<=), (<) :: a -> a -> Bool
  min, max :: a -> a -> a
  
  min x y = 
    case x <= y of
      True -> x
      False -> y
  
  max x y = 
    case x <= y of
      True -> y
      False -> x
      
prop_ord_leq_ref x = x <= x === True
prop_ord_leq_unsym x y = 
  case x <= y of
    False -> y <= x === True
prop_ord_leq_trn x y z = 
  case x <= y of
    True -> case y <= z of
      True -> x <= z === True
prop_ord_max_sym x y =
  max x y === max y x
prop_ord_max_assoc x y z =
  max x (max y z) === max (max x y) z
    
{-# INLINE prop_ord_leq_unsym #-}
{-# INLINE prop_ord_leq_ref #-}
{-# INLINE prop_ord_leq_trn #-}
{-# INLINE prop_ord_max_sym #-}
{-# INLINE prop_ord_max_assoc #-}

      
-- Type class for numbers

class Eq a => Num a where
  (+), (-), (*) :: a -> a -> a

prop_num_add_sym x y = 
  x + y === y + x
prop_num_add_assoc x y z = 
  x + (y + z) === (x + y) + z
prop_num_minus_add1 x y z =
  (x - y) - z === x - (y + z)
prop_num_minus_add2 x y =
  (x + y) - y === x
prop_num_mul_add x y z = 
  x * (y + z) === (x * y) + (x * z)
prop_num_mul_sym x y = 
  x * y === y * x
prop_num_mul_assoc x y z =
  x * (y * z) === (x * y) * z
  
{-# INLINE prop_num_add_sym #-}
{-# INLINE prop_num_add_assoc #-}
{-# INLINE prop_num_minus_add1 #-}
{-# INLINE prop_num_minus_add2 #-}
{-# INLINE prop_num_mul_add #-}
{-# INLINE prop_num_mul_sym #-}
{-# INLINE prop_num_mul_assoc #-}


-- Type class for monoids

class Monoid a where
  mempty :: a
  mappend :: a -> a -> a
  
  mconcat :: [a] -> a
  mconcat = foldr mappend mempty
  
prop_monoid_left x =
  mempty `mappend` x === x
prop_monoid_right x =
  x `mappend` mempty === x
prop_monoid_assoc x y z =
  x `mappend` (y `mappend` z) ===
    (x `mappend` y) `mappend` z
    
{-# INLINE prop_monoid_left #-}
{-# INLINE prop_monoid_right #-}
{-# INLINE prop_monoid_assoc #-}

  
-- Purely polymorphic functions
  
id :: a -> a
id x = x
  
{-# NOINLINE const #-}
const :: a -> b -> a
const x _ = x

(.) :: (b -> c) -> (a -> b) -> a -> c
(f . g) x = f (g x)

-- Boolean functions

not :: Bool -> Bool
not True = False
not False = True

(&&) :: Bool -> Bool -> Bool
True  && x = x
False && _ = False

(||) :: Bool -> Bool -> Bool
False || x = x
True  || _ = True

prop_demorgans_law1 x y = 
  not (x && y) === not x || not y
prop_demorgans_law2 x y =
  not (x || y) === not x && not y

  
-- Natural numbers
  
instance Eq Nat where
  Zero    == Zero    = True
  Zero    == _       = False
  (Suc _) == Zero    = False
  (Suc x) == (Suc y) = x == y
  
prop_nat_eq_ref :: Nat -> Lemma Bool
prop_nat_eq_sym :: Nat -> Nat -> Lemma Bool
prop_nat_eq_trn :: Nat -> Nat -> Nat -> Lemma Bool

prop_nat_eq_ref = prop_eq_eq_ref
prop_nat_eq_sym = prop_eq_eq_sym
prop_nat_eq_trn = prop_eq_eq_trn

  
instance Ord Nat where
  Zero    <= _       = True
  (Suc x) <= Zero    = False
  (Suc x) <= (Suc y) = x <= y

  _       < Zero    = False
  Zero    < _       = True
  (Suc x) < (Suc y) = x < y
  
  min Zero    _       = Zero
  min (Suc x) Zero    = Zero
  min (Suc x) (Suc y) = Suc (min x y)
  
  max Zero x          = x
  max x Zero          = x
  max (Suc x) (Suc y) = Suc (max x y)
  
prop_nat_leq_ref :: Nat -> Lemma Bool
prop_nat_leq_unsym :: Nat -> Nat -> Lemma Bool
prop_nat_leq_trn :: Nat -> Nat -> Nat -> Lemma Bool
prop_nat_max_sym :: Nat -> Nat -> Lemma Nat
prop_nat_max_assoc :: Nat -> Nat -> Nat -> Lemma Nat

prop_nat_leq_ref = prop_ord_leq_ref
prop_nat_leq_unsym = prop_ord_leq_unsym
prop_nat_leq_trn = prop_ord_leq_trn
prop_nat_max_sym = prop_ord_max_sym
prop_nat_max_assoc = prop_ord_max_assoc
  
  
instance Num Nat where
  Zero    + y = y
  (Suc x) + y = Suc (x + y)
  
  Zero    * _ = Zero
  (Suc x) * y = y + (x * y)
  
  Zero    - _       = Zero
  x       - Zero    = x
  (Suc x) - (Suc y) = x - y 
  
prop_nat_add_sym :: Nat -> Nat -> Lemma Nat
prop_nat_add_assoc :: Nat -> Nat -> Nat -> Lemma Nat
prop_nat_minus_add1 :: Nat -> Nat -> Nat -> Lemma Nat
prop_nat_minus_add2 :: Nat -> Nat -> Lemma Nat
prop_nat_mul_add :: Nat -> Nat -> Nat -> Lemma Nat
prop_nat_mul_sym :: Nat -> Nat -> Lemma Nat
prop_nat_mul_assoc :: Nat -> Nat -> Nat -> Lemma Nat

prop_nat_add_sym = prop_num_add_sym
prop_nat_add_assoc = prop_num_add_assoc
prop_nat_minus_add1 = prop_num_minus_add1
prop_nat_minus_add2 = prop_num_minus_add2
prop_nat_mul_add = prop_num_mul_add
prop_nat_mul_sym = prop_num_mul_sym
prop_nat_mul_assoc = prop_num_mul_assoc

prop_nat_leq_add (x :: Nat) (y :: Nat) = 
  x <= (y + x) === True
  
prop_nat_leq_suc (x :: Nat) (y :: Nat) =
  case Suc x <= y of
    True -> x <= y === True
  
even :: Nat -> Bool
even Zero = True
even (Suc Zero) = False
even (Suc (Suc x)) = even x

odd :: Nat -> Bool
odd Zero = False
odd (Suc Zero) = True
odd (Suc (Suc x)) = odd x

prop_even_double x = 
  even (x * (Suc (Suc Zero))) === True
prop_odd_suc_double x =
  odd (Suc (x * (Suc (Suc Zero)))) === True
  
  
-- Integers
  
data Sign = Pos | Neg
data Int  = Int Sign Nat

instance Eq Int where
  Int _ Zero == Int _ Zero = True
  Int Pos x  == Int Pos y  = x == y
  Int Neg x  == Int Neg y  = x == y
  _          == _          = False
  
prop_int_eq_ref :: Int -> Lemma Bool
prop_int_eq_sym :: Int -> Int -> Lemma Bool
prop_int_eq_trn :: Int -> Int -> Int -> Lemma Bool

prop_int_eq_ref = prop_eq_eq_ref
prop_int_eq_sym = prop_eq_eq_sym
prop_int_eq_trn = prop_eq_eq_trn


instance Ord Int where
  Int _ Zero <= Int _ Zero = True
  Int Pos x  <= Int Pos y  = x <= y
  Int Neg x  <= Int Neg y  = y <= x
  Int Neg _  <= Int Pos _  = True
  Int Pos _  <= Int Neg _  = False

prop_int_leq_ref :: Int -> Lemma Bool
prop_int_leq_unsym :: Int -> Int -> Lemma Bool
prop_int_leq_trn :: Int -> Int -> Int -> Lemma Bool

prop_int_leq_ref = prop_ord_leq_ref
prop_int_leq_unsym = prop_ord_leq_unsym
prop_int_leq_trn = prop_ord_leq_trn


instance Num Int where
  Int Pos x       + Int Pos y       = Int Pos (x + y)
  Int Neg x       + Int Neg y       = Int Neg (x + y)
  Int Pos (Suc x) + Int Neg (Suc y) = Int Pos x + Int Neg y
  Int Neg (Suc x) + Int Pos (Suc y) = Int Neg x + Int Pos y
  Int _   Zero    + y               = y
  x               + Int _   Zero    = x
  
prop_int_add_sym :: Int -> Int -> Lemma Int
prop_int_add_assoc :: Int -> Int -> Int -> Lemma Int
 
prop_int_add_sym = prop_num_add_sym
prop_int_add_assoc = prop_num_add_assoc
  
-- Lists

instance Monoid [a] where
  mempty = []
  mappend = (++)
  
prop_list_monoid_right :: [a] -> Lemma [a]
prop_list_monoid_left :: [a] -> Lemma [a]
prop_list_monoid_assoc :: [a] -> [a] -> [a] -> Lemma [a]

prop_list_monoid_right = prop_monoid_right
prop_list_monoid_left = prop_monoid_left
prop_list_monoid_assoc = prop_monoid_assoc


null :: [a] -> Bool
null [] = True
null _  = False
  
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ b [] = b
foldr f b (a:as) = f a (foldr f b as)

reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]

reverse2 :: [a] -> [a] -> [a]
reverse2 [] ys = ys
reverse2 (x:xs) ys = reverse2 xs (x:ys)

zip :: [a] -> [b] -> [(a, b)]
zip [] _ = []
zip _ [] = []
zip (x:xs) (y:ys) = (x, y) : (zip xs ys)

remove :: Nat -> [Nat] -> [Nat]
remove _ [] = []
remove n (x:xs) = 
  case n == x of
    True -> remove n xs
    False -> x : (remove n xs)
    
length :: [a] -> Nat
length [] = Zero
length (_:xs) = Suc (length xs)

minimum :: [Nat] -> Nat
minimum [] = Zero
minimum [x] = x
minimum (x:xs) =
  case x <= (minimum xs) of
    True -> x
    False -> minimum xs
    
elem :: Nat -> [Nat] -> Bool
elem _ [] = False
elem n (x:xs) = 
  case n == x of
    True -> True
    False -> elem n xs

drop :: Nat -> [a] -> [a]
drop Zero xs = xs
drop _ [] = []
drop (Suc x) (_:xs) = drop x xs

take :: Nat -> [a] -> [a]
take Zero _ = []
take _ [] = []
take (Suc x) (y:ys) = y:(take x ys) 

count :: Nat -> [Nat] -> Nat
count x [] = Zero
count x (y:ys) =
  case x == y of
    True -> Suc (count x ys)
    False -> count x ys

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = (f x) : (map f xs)

takeWhile :: (a -> Bool) -> [a] -> [a]
takeWhile _ [] = []
takeWhile p (x:xs) = 
  case p x of
    True -> x : (takeWhile p xs)
    False -> []
    
dropWhile :: (a -> Bool) -> [a] -> [a]
dropWhile _ [] = []
dropWhile p (x:xs) =
  case p x of
    True -> dropWhile p xs
    False -> x:xs
    
filter :: (a -> Bool) -> [a] -> [a]
filter _ [] = []
filter p (x:xs) = 
  case p x of
    True -> x : (filter p xs)
    False -> filter p xs

    
-- List function properties

prop_reverse_idem xs = 
  reverse (reverse xs) === xs 
prop_reverse_count x xs =
  count x xs === count x (reverse xs)
prop_reverse_filter p xs =
  filter p (reverse xs) === reverse (filter p xs)
  
prop_map_filter f p xs =
  map f (filter (p . f) xs) === filter p (map f xs)
prop_map_take f n xs =
  take n (map f xs) === map f (take n xs)
prop_map_drop f n xs =
  drop n (map f xs) === map f (drop n xs)
prop_map_comp f g xs =
  map f (map g xs) === map (f . g) xs
  
prop_drop_none xs = 
  dropWhile (const False) xs === xs
prop_take_all xs =
  takeWhile (const True) xs === xs
prop_takedropwhile p xs =
  takeWhile p xs ++ dropWhile p xs === xs
  
prop_takedrop n m xs =
  take n (drop m xs) === drop m (take (n + m) xs)
prop_droptake n m xs = 
  drop n (take m xs) === take (m - n) (drop n xs)
prop_dropadd n m xs = 
  drop n (drop m xs) === drop (n + m) xs
prop_takeminus n m xs =
  take n (take m xs) === take (min n m) xs
prop_dropappend n xs ys =
  drop n (xs ++ ys) === drop n xs ++ drop (n - length xs) ys
  
prop_length_filter p xs =
  length (filter p xs) <= length xs === True
prop_length_drop n xs =
  length (drop n xs) === length xs - n
prop_length_map f xs =
  length xs === length (map f xs)  
prop_length_take n xs =
  length (take n xs) === n `min` (length xs)
prop_length_remove x xs = 
  length (remove x xs) <= length xs === True
  
prop_elem_append1 x xs ys =
  case x `elem` xs of
    True -> x `elem` (xs ++ ys) === True
prop_elem_append2 x xs ys =
  case x `elem` ys of
    True -> x `elem` (xs ++ ys) === True
prop_elem_minimum x xs = 
  case elem x xs of
    True -> minimum xs <= x === True
    
prop_count_append1 n x xs =
  case n == x of
    False -> count n xs === count n (xs ++ [x])
prop_count_append2 n xs ys =
  case elem n ys of
    False -> count n xs === count n (xs ++ ys)
prop_count_append3 n xs ys =
  count n xs + count n ys === count n (xs ++ ys)
  
prop_zip_append1 xs ys zs = 
  (xs ++ ys) `zip` zs === zip xs (take (length xs) zs) ++ zip ys (drop (length xs) zs)
prop_zip_append2 xs ys zs =
  zip xs (ys ++ zs) === zip (take (length ys) xs) ys ++ zip (drop (length ys) xs) zs

  
-- Sorting 

sorted :: [Nat] -> Bool
sorted [] = True
sorted [x] = True
sorted (x:y:ys) = 
  case x <= y of
    False -> False
    True -> sorted (y:ys)
   
  
-- Insertion sort
  
insert :: Nat -> [Nat] -> [Nat]
insert n [] = [n]
insert n (x:xs) =
  case n <= x of
    True -> n:x:xs
    False -> x : (insert n xs)

insertsort :: [Nat] -> [Nat]
insertsort [] = []
insertsort (x:xs) = insert x (insertsort xs)

prop_verify_insert1 x xs = 
  elem x (insert x xs) === True
prop_verify_insert2 x xs = 
  length (insert x xs) === Suc (length xs)

prop_sorting_insert x xs =
  case sorted xs of 
    True -> sorted (insert x xs) === True 

prop_verify_insertsort xs =
  sorted (insertsort xs) === True
  
prop_insertsort_count x xs =
  count x xs === count x (insertsort xs)
prop_insertsort_elem x xs =
  elem x (insertsort xs) === elem x xs


-- Quicksort

leqX :: Nat -> Nat -> Bool
leqX x y = y <= x

notLeqX :: Nat -> Nat -> Bool
notLeqX x y = not (y <= x)

quicksort :: [Nat] -> [Nat]
quicksort [] = []
quicksort [x] = [x]
quicksort (x:xs) = 
  quicksort (filter (leqX x) xs) ++ [x] ++ quicksort (filter (notLeqX x) xs)
  
prop_verify_quicksort xs =
  sorted (quicksort xs) === True
  

-- Properties I'm working on

prop_reverse2_idem xs =
  reverse2 (reverse2 xs []) [] === xs


-- Properties Zeno cannot prove

prop_takelenrev x xs =
  take (length xs) (reverse xs) === take (length xs) (reverse xs ++ [x])
prop_lenrevzip xs ys =
  case length xs == length ys of
    True -> zip (reverse xs) (reverse ys) === reverse (zip xs ys)
prop_revdrop n xs =
  reverse (drop n xs) === take ((length xs) - n) (reverse xs)
